D:Dsys.
Feasible(D)
 (dec:(i,a:IdM(i).state(?if a  dom(M(i).prob) then Outcome else Void fi )), i:Id.
 d-machine(i;M(i);dec(i))
  w-automaton(x.M(i).ds(x);a.M(i).da(locl(a));l,tg. M(source(l)).dout(l,tg))) 

latex

Definitions

t  T, {T}, P  Q, x:A. B(x), SQType(T), s = t, , Id, s ~ t, Atom$n, M.dout(l,tg), x:AB(x), x:A  B(x), <a, b>, P & Q, P  Q, b, {x:A| B(x)} , IdLnk, x. t(x), t.1, Type, Msg(M), Msg(da), type List, State(ds), M.state, M.ds(x), M.sends(k,s,v), f(a), S  T, filter(P;l), Feasible(D), M.da(a), A, , Unit, left + right, lnk(k), islocal(k), tag(k), act(k), kindcase(k; a.f(a); l,t.g(l;t) ), locl(a), Knd, if b then t else f fi , destination(l), p q, timedState(ds), , read-state(s), M.ef(k,x,s,v)?w, Dsys, finite-type(T), Feasible(M), , False, ma-prob-da-dom(M;b), Void, A  B, , Outcome, suptype(S; T), d-machine(i;M;dec), w-automaton(T;TA;M), mlnk(m), source(l), a = b, x.A(x), M(i), M.Msg, M.(timed)state, ma-prob-da(M)

Lemmas

ma-ef-val wf, read-state wf, bor wf, ldst wf, lnk wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, filter wf, ma-send-val wf, filter type, mlnk wf d, subtype rel list, assert wf, eq id wf, pi1 wf, assert-eq-id, ma-dout wf, d-m wf, lsrc wf, Id sq